\begin{tabbing}
$\forall$${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$\mathbb{B}$)\} .
\\[0ex](($x$ when $e$) = tt $\in$ $\mathbb{B}$)
\\[0ex]$\Rightarrow$ (($x$ initially@loc($e$)  = ff $\in$ $\mathbb{B}$) $\vee$ ($\exists$${\it e'}$:E. (${\it e'}$ $\leq$loc $e$  \& ($x$ when ${\it e'}$) = ff $\in$ $\mathbb{B}$)))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex]((${\it e'}$ $<$loc $e$)
\\[0ex]\& ($x$ when ${\it e'}$) = ff $\in$ $\mathbb{B}$
\\[0ex]\& ($x$ after ${\it e'}$) = tt $\in$ $\mathbb{B}$
\\[0ex]\& $\forall$${\it e''}$$\in$(${\it e'}$,$e$].($x$ when ${\it e''}$) = tt $\in$ $\mathbb{B}$
\\[0ex]\& $\forall$${\it e''}$$\in$[${\it e'}$,$e$).($x$ after ${\it e''}$) = tt $\in$ $\mathbb{B}$))
\-
\end{tabbing}